Certified Absence of Dangling Pointers in a Language with Explicit Deallocation
Identifieur interne : 003111 ( Main/Exploration ); précédent : 003110; suivant : 003112Certified Absence of Dangling Pointers in a Language with Explicit Deallocation
Auteurs : Javier De Dios [Espagne] ; Manuel Montenegro [Espagne] ; Ricardo Pe A [Espagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Safe is a first-order eager functional language with facilities for programmer controlled destruction of data structures. It provides also regions, i.e. disjoint parts of the heap, where the program allocates data structures, so that the runtime system does not need a garbage collector. A region is a collection of cells, each one big enough to allocate a data constructor. Deallocating cells or regions may create dangling pointers. The language is aimed at inferring and certifying memory safety properties in a Proof Carrying Code like environment. Some of its analyses have been presented elsewhere. The one relevant to this paper is a type system and a type inference algorithm guaranteeing that well-typed programs will be free of dangling pointers at runtime. Here we present how to generate formal certificates about the absence of dangling pointers property inferred by the compiler. The certificates are Isabelle/HOL proof scripts which can be proof-checked by this tool when loaded with a database of previously proved theorems. The key idea is proving an Isabelle/HOL theorem for each syntactic construction of the language, relating the static types inferred by the compiler to the dynamic properties about the heap that will be satisfied at runtime.
Url:
DOI: 10.1007/978-3-642-16265-7_22
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001895
- to stream Istex, to step Curation: 001876
- to stream Istex, to step Checkpoint: 000873
- to stream Main, to step Merge: 003168
- to stream Main, to step Curation: 003111
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Certified Absence of Dangling Pointers in a Language with Explicit Deallocation</title><author><name sortKey="De Dios, Javier" sort="De Dios, Javier" uniqKey="De Dios J" first="Javier" last="De Dios">Javier De Dios</name></author><author><name sortKey="Montenegro, Manuel" sort="Montenegro, Manuel" uniqKey="Montenegro M" first="Manuel" last="Montenegro">Manuel Montenegro</name></author><author><name sortKey="Pe A, Ricardo" sort="Pe A, Ricardo" uniqKey="Pe A R" first="Ricardo" last="Pe A">Ricardo Pe A</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:6B063B9E2D14A0940CEEE1B4E0176F40888C8440</idno><date when="2010" year="2010">2010</date><idno type="doi">10.1007/978-3-642-16265-7_22</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-MX0N5CLV-5/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001895</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001895</idno><idno type="wicri:Area/Istex/Curation">001876</idno><idno type="wicri:Area/Istex/Checkpoint">000873</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000873</idno><idno type="wicri:doubleKey">0302-9743:2010:De Dios J:certified:absence:of</idno><idno type="wicri:Area/Main/Merge">003168</idno><idno type="wicri:Area/Main/Curation">003111</idno><idno type="wicri:Area/Main/Exploration">003111</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Certified Absence of Dangling Pointers in a Language with Explicit Deallocation</title><author><name sortKey="De Dios, Javier" sort="De Dios, Javier" uniqKey="De Dios J" first="Javier" last="De Dios">Javier De Dios</name><affiliation wicri:level="4"><orgName type="university">Université complutense de Madrid</orgName><country>Espagne</country><placeName><settlement type="city">Madrid</settlement><region nuts="2" type="region">Communauté de Madrid</region></placeName></affiliation><affiliation></affiliation></author><author><name sortKey="Montenegro, Manuel" sort="Montenegro, Manuel" uniqKey="Montenegro M" first="Manuel" last="Montenegro">Manuel Montenegro</name><affiliation wicri:level="4"><orgName type="university">Université complutense de Madrid</orgName><country>Espagne</country><placeName><settlement type="city">Madrid</settlement><region nuts="2" type="region">Communauté de Madrid</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Espagne</country></affiliation></author><author><name sortKey="Pe A, Ricardo" sort="Pe A, Ricardo" uniqKey="Pe A R" first="Ricardo" last="Pe A">Ricardo Pe A</name><affiliation wicri:level="4"><orgName type="university">Université complutense de Madrid</orgName><country>Espagne</country><placeName><settlement type="city">Madrid</settlement><region nuts="2" type="region">Communauté de Madrid</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Espagne</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Safe is a first-order eager functional language with facilities for programmer controlled destruction of data structures. It provides also regions, i.e. disjoint parts of the heap, where the program allocates data structures, so that the runtime system does not need a garbage collector. A region is a collection of cells, each one big enough to allocate a data constructor. Deallocating cells or regions may create dangling pointers. The language is aimed at inferring and certifying memory safety properties in a Proof Carrying Code like environment. Some of its analyses have been presented elsewhere. The one relevant to this paper is a type system and a type inference algorithm guaranteeing that well-typed programs will be free of dangling pointers at runtime. Here we present how to generate formal certificates about the absence of dangling pointers property inferred by the compiler. The certificates are Isabelle/HOL proof scripts which can be proof-checked by this tool when loaded with a database of previously proved theorems. The key idea is proving an Isabelle/HOL theorem for each syntactic construction of the language, relating the static types inferred by the compiler to the dynamic properties about the heap that will be satisfied at runtime.</div></front></TEI><affiliations><list><country><li>Espagne</li></country><region><li>Communauté de Madrid</li></region><settlement><li>Madrid</li></settlement><orgName><li>Université complutense de Madrid</li></orgName></list><tree><country name="Espagne"><region name="Communauté de Madrid"><name sortKey="De Dios, Javier" sort="De Dios, Javier" uniqKey="De Dios J" first="Javier" last="De Dios">Javier De Dios</name></region><name sortKey="Montenegro, Manuel" sort="Montenegro, Manuel" uniqKey="Montenegro M" first="Manuel" last="Montenegro">Manuel Montenegro</name><name sortKey="Montenegro, Manuel" sort="Montenegro, Manuel" uniqKey="Montenegro M" first="Manuel" last="Montenegro">Manuel Montenegro</name><name sortKey="Pe A, Ricardo" sort="Pe A, Ricardo" uniqKey="Pe A R" first="Ricardo" last="Pe A">Ricardo Pe A</name><name sortKey="Pe A, Ricardo" sort="Pe A, Ricardo" uniqKey="Pe A R" first="Ricardo" last="Pe A">Ricardo Pe A</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003111 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003111 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:6B063B9E2D14A0940CEEE1B4E0176F40888C8440
|texte= Certified Absence of Dangling Pointers in a Language with Explicit Deallocation
}}
| This area was generated with Dilib version V0.6.33. |  |